T:Type, l:(T List), a,x:T. (x  cons(a; l))  ((x = a)  (x  l)) 

latex

Definitions	False, A, A  B, prop{i:l}, t  T, P  Q, P  Q, P  Q, A c B, x:A. B(x), P  Q, (x  l), P  Q, x:A. B(x), , ff, tt, i <z j, b, i z j, if b then t else f fi , nth_tl(n;as), hd(l), Y, l[i], ||as||, True, T, guard(T), sq_type(T), decidable(P), nequal(T; a; b)
Lemmas	nat wf, select wf, length wf1, neg assert of eq int, nat sq, le wf, assert of eq int, eq int wf, decidable assert, select cons tl, length cons, non neg length, squash wf